Nuprl Lemma : ccpred_wf
11,40
postcript
pdf
id
:Id. ccpred(
id
)
chain_config()
latex
Definitions
ccpred(
id
)
,
chain_config()
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
unit
wf
,
nat
wf
,
Id
wf
origin
id:Id. ccpred(id) 
chain_config() id:Id. ccpred(id) chain_config() Tx:A. B(x)